Nuprl Lemma : trans_functionality_wrt_iff 13,42
T:Type, R, R':(TT).
(x, y:T. R(x,y)  R'(x,y))  (Trans(T;y,x.R(x,y))  Trans(T;y,x.R'(x,y))) 
latex

Uprel 1, rel 1
DefinitionsP  Q, P & Q, t  T, Trans(T;x,y.E(x;y)), x(s1,s2), P  Q, P  Q, , x:A. B(x), x. t(x), x,y. t(x;y), {T}, x(s)
Lemmasiff wf, implies functionality wrt iff, all functionality wrt iff, iff functionality wrt iff, trans wf

origin